\Aufgabe[Computing the (Greatest) Bisimulation Relation \hfill\textbf{(1 Point)}]

Let $K_1 = (S_1, R_1, L_1)$ and  $K_2 = (S_2, R_2, L_2)$ be two Kripke structures over a set of atomic predicates $\mathit{AP}$.
The relations $H_n \subseteq S_1 \times S_2$ are inductively defined by:
\begin{itemize}
\item $(s_1,s_2) \in H_0$ iff $L_1(s_1) = L_2(s_2)$.
\item $(s_1,s_2) \in H_{n+1}$ iff
    \begin{enumerate}[(i)]
    \item $(s_1,s_2) \in H_n$,
    \item for all $(s_1,t_1) \in R_1$ there exists a $(s_2,t_2) \in R_2$ with $(t_1,t_2) \in H_n$, and
    \item for all $(s_2,t_2) \in R_2$ there exists a $(s_1,t_1) \in R_1$ with $(t_1,t_2) \in H_n$.
    \end{enumerate}
\end{itemize}

\begin{enumerate}

	\item Compute the sequence $H_0, H_1, H_2,\ldots$ for the Kripke structures $K_1$ and $K_2$ from Exercise 3.

	\item Show that the sequence $H_0, H_1, H_2,\ldots$ \emph{stabilizes} for all finite Kripke structures $K_1$ and $K_2$, i.e., there is a $n \ge 0$ such that $H_n = H_{n+1}$.

	\item Construct Kripke structures $K_1^n$ and $K_2^n$ such that the sequence $H_0, H_1, H_2,\ldots$ stabilizes after exactly $n$ steps.

\end{enumerate}

\textbf{Solution}

\begin{enumerate}
	\item Compute the sequence $H_0, H_1, H_2,\ldots$ for the Kripke structures $K_1$ and $K_2$ from Exercise 3.\\
	
	$H_0 = \{(s_0, t_0), (s_0, t_5), (s_0, t_{10}), (s_5, t_0), (s_5, t_5), (s_5, t_{10}), (s_9, t_0), (s_9, t_5), (s_9, t_{10}),$\\
	\indent\quad\quad\quad$(s_1, t_1), (s_1, t_6), (s_1, t_7), (s_6, t_1), (s_6, t_6), (s_6, t_7),$\\
	\indent\quad\quad\quad$(s_2, t_2), (s_2, t_4), (s_2, t_8), (s_4, t_2), (s_4, t_4), (s_4, t_8), (s_7, t_2), (s_7, t_4), (s_7, t_8),$\\
	\indent\quad\quad\quad$(s_3, t_3), (s_3, t_9), (s_8, t_3), (s_8, t_9)\}$\\
		
	$H_1 = \{(s_0, t_0), (s_5, t_5), (s_5, t_{10}), (s_9, t_5), (s_9, t_{10}),$\\
	\indent\quad\quad\quad$(s_1, t_1), (s_1, t_6), (s_1, t_7), (s_6, t_1), (s_6, t_6), (s_6, t_7),$\\
	\indent\quad\quad\quad$(s_2, t_2), (s_4, t_4), (s_7, t_8),$\\
	\indent\quad\quad\quad$(s_3, t_3), (s_3, t_9), (s_8, t_3), (s_8, t_9)\}$\\
	
	$H_2 = \{(s_0, t_0), (s_5, t_5), (s_5, t_{10}), (s_9, t_5), (s_9, t_{10}),$\\
	\indent\quad\quad\quad$(s_1, t_1), (s_6, t_6), (s_6, t_7),$\\
	\indent\quad\quad\quad$(s_2, t_2), (s_4, t_4), (s_7, t_8),$\\
	\indent\quad\quad\quad$(s_3, t_3), (s_3, t_9), (s_8, t_3), (s_8, t_9)\}$\\
	
	$H_3 = H_2$\\
	
	\item Show that the sequence $H_0, H_1, H_2,\ldots$ \emph{stabilizes} for all finite Kripke structures $K_1$ and $K_2$, i.e., there is a $n \ge 0$ such that $H_n = H_{n+1}$.\\
	
	For finite Kripke structures, the sets of States $S_1$ and $S_2$ are finite and, therefore, each $H_n$ has to be finite as well. 
	From the definition of $H_{n+1}$ we can follow that $|H_n| \ge |H_{n+1}|$ for all $n \ge 0$, i.e. by construction we never add any new element, we only are able to remove elements from $H_n$ which violate the conditions (ii) or (iii).
	Since $H_0$ is finite, we are only able to remove finite many elements during the construction of $H_{n+1}$.
	Therefore it always is possible to find a constant $n \ge 0$ so that $H_{n} = H_{n+1}$.
\end{enumerate}
